『Homotopy Type Theory: Univalent Foundations of Mathematics』Chapter 2 Homotopy type theory
『Homotopy Type Theory: Univalent Foundations of Mathematics』Chapter 1 Type theory ←
→ 『Homotopy Type Theory: Univalent Foundations of Mathematics』Chapter 3 Sets and logic
P59-P106
連続写像$ f: X → Y 、$ g: X → Y があって、連続写像$ H: X \times [0, 1] は$ H(x, 0) = f(x) 、$ H(x, 1) = g(x) を満たす。
$ [0, 1] : 閉区間0~1。閉区間は端っこ(境界)を含まない区間。
$ X, Y は$ X \simeq Y (ホモトピー同値)
連続写像$ H をホモトピーと呼ぶ
ホモトピー同値な空間は、同じ代数的不変量(ホモロジーや基本群など)を持ち、同じホモトピー型を持つという
ホモトピック、∞-グルーポイド
table:訳
英語 日本語
endpoint-preserving
rel endpoints
algebraic invariants 代数的不変量
homotopy equivalent ホモトピー同値
table:k-morphism
対象?
0-dimension 対象
1-dimension パス間
2-dimensional path ホモトピー
3-dimensional
ホモトピー群
$ \pi_1 = (X, x_0)
空間$ X 、基点$ x_0
基本群
$ \pi_2 = (X, x_0)
$ \pi_3 = (X, x_0)
ホモトピー間のホモトピー類の群?